<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue1062</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\nonstopmode
\documentclass{article}

\usepackage{agda}

\begin{document}
</a><a id="75" class="Markup">\begin{code}</a>

<a id="89" class="Symbol">{-#</a> <a id="93" class="Keyword">OPTIONS</a> <a id="101" class="Pragma">--copatterns</a> <a id="114" class="Pragma">--sized-types</a> <a id="128" class="Symbol">#-}</a>

<a id="133" class="Symbol">{-#</a> <a id="137" class="Keyword">BUILTIN</a> <a id="145" class="Keyword">SIZE</a>    <a id="Size"></a><a id="153" href="Issue1062.html#153" class="Postulate">Size</a>   <a id="160" class="Symbol">#-}</a>
<a id="164" class="Symbol">{-#</a> <a id="168" class="Keyword">BUILTIN</a> <a id="176" class="Keyword">SIZELT</a>  <a id="Size&lt;_"></a><a id="184" href="Issue1062.html#184" class="Postulate Operator">Size&lt;_</a> <a id="191" class="Symbol">#-}</a>
<a id="195" class="Symbol">{-#</a> <a id="199" class="Keyword">BUILTIN</a> <a id="207" class="Keyword">SIZESUC</a> <a id="↑_"></a><a id="215" href="Issue1062.html#215" class="Postulate Operator">↑_</a>     <a id="222" class="Symbol">#-}</a>
<a id="226" class="Symbol">{-#</a> <a id="230" class="Keyword">BUILTIN</a> <a id="238" class="Keyword">SIZEINF</a> <a id="∞"></a><a id="246" href="Issue1062.html#246" class="Postulate">∞</a>      <a id="253" class="Symbol">#-}</a>

<a id="258" class="Keyword">data</a> <a id="List"></a><a id="263" href="Issue1062.html#263" class="Datatype">List</a> <a id="268" class="Symbol">(</a><a id="269" href="Issue1062.html#269" class="Bound">A</a> <a id="271" class="Symbol">:</a> <a id="273" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="276" class="Symbol">)</a> <a id="278" class="Symbol">:</a> <a id="280" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="284" class="Keyword">where</a>
  <a id="List.[]"></a><a id="292" href="Issue1062.html#292" class="InductiveConstructor">[]</a> <a id="295" class="Symbol">:</a> <a id="297" href="Issue1062.html#263" class="Datatype">List</a> <a id="302" href="Issue1062.html#269" class="Bound">A</a>
  <a id="List._∷_"></a><a id="306" href="Issue1062.html#306" class="InductiveConstructor Operator">_∷_</a> <a id="310" class="Symbol">:</a> <a id="312" class="Symbol">(</a><a id="313" href="Issue1062.html#313" class="Bound">x</a> <a id="315" class="Symbol">:</a> <a id="317" href="Issue1062.html#269" class="Bound">A</a><a id="318" class="Symbol">)</a> <a id="320" class="Symbol">(</a><a id="321" href="Issue1062.html#321" class="Bound">xs</a> <a id="324" class="Symbol">:</a> <a id="326" href="Issue1062.html#263" class="Datatype">List</a> <a id="331" href="Issue1062.html#269" class="Bound">A</a><a id="332" class="Symbol">)</a> <a id="334" class="Symbol">-&gt;</a> <a id="337" href="Issue1062.html#263" class="Datatype">List</a> <a id="342" href="Issue1062.html#269" class="Bound">A</a>

<a id="345" class="Keyword">record</a> <a id="_×_"></a><a id="352" href="Issue1062.html#352" class="Record Operator">_×_</a> <a id="356" class="Symbol">(</a><a id="357" href="Issue1062.html#357" class="Bound">A</a> <a id="359" href="Issue1062.html#359" class="Bound">B</a> <a id="361" class="Symbol">:</a> <a id="363" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="366" class="Symbol">)</a> <a id="368" class="Symbol">:</a> <a id="370" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="374" class="Keyword">where</a>
  <a id="382" class="Keyword">constructor</a> <a id="_,_"></a><a id="394" href="Issue1062.html#394" class="InductiveConstructor Operator">_,_</a>
  <a id="400" class="Keyword">field</a>
    <a id="_×_.fst"></a><a id="410" href="Issue1062.html#410" class="Field">fst</a> <a id="414" class="Symbol">:</a> <a id="416" href="Issue1062.html#357" class="Bound">A</a>
    <a id="_×_.snd"></a><a id="422" href="Issue1062.html#422" class="Field">snd</a> <a id="426" class="Symbol">:</a> <a id="428" href="Issue1062.html#359" class="Bound">B</a>
<a id="430" class="Keyword">open</a> <a id="435" href="Issue1062.html#352" class="Module Operator">_×_</a>

<a id="440" class="Comment">-- Sized streams via head/tail.</a>

<a id="473" class="Keyword">record</a> <a id="Stream"></a><a id="480" href="Issue1062.html#480" class="Record">Stream</a> <a id="487" class="Symbol">{</a><a id="488" href="Issue1062.html#488" class="Bound">i</a> <a id="490" class="Symbol">:</a> <a id="492" href="Issue1062.html#153" class="Postulate">Size</a><a id="496" class="Symbol">}</a> <a id="498" class="Symbol">(</a><a id="499" href="Issue1062.html#499" class="Bound">A</a> <a id="501" class="Symbol">:</a> <a id="503" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="506" class="Symbol">)</a> <a id="508" class="Symbol">:</a> <a id="510" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="514" class="Keyword">where</a>
  <a id="522" class="Keyword">coinductive</a><a id="533" class="Symbol">;</a> <a id="535" class="Keyword">constructor</a> <a id="_∷_"></a><a id="547" href="Issue1062.html#547" class="CoinductiveConstructor Operator">_∷_</a>
  <a id="553" class="Keyword">field</a>
    <a id="Stream.head"></a><a id="563" href="Issue1062.html#563" class="Field">head</a>  <a id="569" class="Symbol">:</a> <a id="571" href="Issue1062.html#499" class="Bound">A</a>
    <a id="Stream.tail"></a><a id="577" href="Issue1062.html#577" class="Field">tail</a>  <a id="583" class="Symbol">:</a> <a id="585" class="Symbol">∀</a> <a id="587" class="Symbol">{</a><a id="588" href="Issue1062.html#588" class="Bound">j</a> <a id="590" class="Symbol">:</a> <a id="592" href="Issue1062.html#184" class="Postulate Operator">Size&lt;</a> <a id="598" href="Issue1062.html#488" class="Bound">i</a><a id="599" class="Symbol">}</a> <a id="601" class="Symbol">→</a> <a id="603" href="Issue1062.html#480" class="Record">Stream</a> <a id="610" class="Symbol">{</a><a id="611" href="Issue1062.html#588" class="Bound">j</a><a id="612" class="Symbol">}</a> <a id="614" href="Issue1062.html#499" class="Bound">A</a>
<a id="616" class="Keyword">open</a> <a id="621" href="Issue1062.html#480" class="Module">Stream</a> <a id="628" class="Keyword">public</a>

<a id="_∷ˢ_"></a><a id="636" href="Issue1062.html#636" class="Function Operator">_∷ˢ_</a> <a id="641" class="Symbol">:</a> <a id="643" class="Symbol">∀</a> <a id="645" class="Symbol">{</a><a id="646" href="Issue1062.html#646" class="Bound">i</a> <a id="648" href="Issue1062.html#648" class="Bound">A</a><a id="649" class="Symbol">}</a> <a id="651" class="Symbol">→</a> <a id="653" href="Issue1062.html#648" class="Bound">A</a> <a id="655" class="Symbol">→</a> <a id="657" href="Issue1062.html#480" class="Record">Stream</a> <a id="664" class="Symbol">{</a><a id="665" href="Issue1062.html#646" class="Bound">i</a><a id="666" class="Symbol">}</a> <a id="668" href="Issue1062.html#648" class="Bound">A</a> <a id="670" class="Symbol">→</a> <a id="672" href="Issue1062.html#480" class="Record">Stream</a> <a id="679" class="Symbol">{</a><a id="680" href="Issue1062.html#215" class="Postulate Operator">↑</a> <a id="682" href="Issue1062.html#646" class="Bound">i</a><a id="683" class="Symbol">}</a> <a id="685" href="Issue1062.html#648" class="Bound">A</a>
<a id="687" href="Issue1062.html#563" class="Field">head</a>  <a id="693" class="Symbol">(</a><a id="694" href="Issue1062.html#694" class="Bound">a</a> <a id="696" href="Issue1062.html#636" class="Function Operator">∷ˢ</a> <a id="699" href="Issue1062.html#699" class="Bound">as</a><a id="701" class="Symbol">)</a> <a id="703" class="Symbol">=</a> <a id="705" href="Issue1062.html#694" class="Bound">a</a>
<a id="707" href="Issue1062.html#577" class="Field">tail</a>  <a id="713" class="Symbol">(</a><a id="714" href="Issue1062.html#714" class="Bound">a</a> <a id="716" href="Issue1062.html#636" class="Function Operator">∷ˢ</a> <a id="719" href="Issue1062.html#719" class="Bound">as</a><a id="721" class="Symbol">)</a> <a id="723" class="Symbol">=</a> <a id="725" href="Issue1062.html#719" class="Bound">as</a>

<a id="729" class="Comment">-- Streams and lists.</a>

<a id="752" class="Comment">-- Prepending a list to a stream.</a>

<a id="_++ˢ_"></a><a id="787" href="Issue1062.html#787" class="Function Operator">_++ˢ_</a> <a id="793" class="Symbol">:</a> <a id="795" class="Symbol">∀</a> <a id="797" class="Symbol">{</a><a id="798" href="Issue1062.html#798" class="Bound">i</a> <a id="800" href="Issue1062.html#800" class="Bound">A</a><a id="801" class="Symbol">}</a> <a id="803" class="Symbol">→</a> <a id="805" href="Issue1062.html#263" class="Datatype">List</a> <a id="810" href="Issue1062.html#800" class="Bound">A</a> <a id="812" class="Symbol">→</a> <a id="814" href="Issue1062.html#480" class="Record">Stream</a> <a id="821" class="Symbol">{</a><a id="822" href="Issue1062.html#798" class="Bound">i</a><a id="823" class="Symbol">}</a> <a id="825" href="Issue1062.html#800" class="Bound">A</a> <a id="827" class="Symbol">→</a> <a id="829" href="Issue1062.html#480" class="Record">Stream</a> <a id="836" class="Symbol">{</a><a id="837" href="Issue1062.html#798" class="Bound">i</a><a id="838" class="Symbol">}</a> <a id="840" href="Issue1062.html#800" class="Bound">A</a>
<a id="842" href="Issue1062.html#292" class="InductiveConstructor">[]</a>        <a id="852" href="Issue1062.html#787" class="Function Operator">++ˢ</a> <a id="856" href="Issue1062.html#856" class="Bound">s</a> <a id="858" class="Symbol">=</a> <a id="860" href="Issue1062.html#856" class="Bound">s</a>
<a id="862" class="Symbol">(</a><a id="863" href="Issue1062.html#863" class="Bound">a</a> <a id="865" href="Issue1062.html#306" class="InductiveConstructor Operator">∷</a> <a id="867" href="Issue1062.html#867" class="Bound">as</a><a id="869" class="Symbol">)</a>  <a id="872" href="Issue1062.html#787" class="Function Operator">++ˢ</a> <a id="876" href="Issue1062.html#876" class="Bound">s</a> <a id="878" class="Symbol">=</a> <a id="880" href="Issue1062.html#863" class="Bound">a</a> <a id="882" href="Issue1062.html#636" class="Function Operator">∷ˢ</a> <a id="885" class="Symbol">(</a><a id="886" href="Issue1062.html#867" class="Bound">as</a> <a id="889" href="Issue1062.html#787" class="Function Operator">++ˢ</a> <a id="893" href="Issue1062.html#876" class="Bound">s</a><a id="894" class="Symbol">)</a>

<a id="897" class="Comment">-- Unfold which produces several outputs at one step</a>

<a id="951" class="Keyword">record</a> <a id="List1"></a><a id="958" href="Issue1062.html#958" class="Record">List1</a> <a id="964" class="Symbol">(</a><a id="965" href="Issue1062.html#965" class="Bound">A</a> <a id="967" class="Symbol">:</a> <a id="969" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="972" class="Symbol">)</a> <a id="974" class="Symbol">:</a> <a id="976" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="980" class="Keyword">where</a>
  <a id="988" class="Keyword">constructor</a> <a id="_∷_"></a><a id="1000" href="Issue1062.html#1000" class="InductiveConstructor Operator">_∷_</a>
  <a id="1006" class="Keyword">field</a>
    <a id="List1.head"></a><a id="1016" href="Issue1062.html#1016" class="Field">head</a>  <a id="1022" class="Symbol">:</a> <a id="1024" href="Issue1062.html#965" class="Bound">A</a>
    <a id="List1.tail"></a><a id="1030" href="Issue1062.html#1030" class="Field">tail</a>  <a id="1036" class="Symbol">:</a> <a id="1038" href="Issue1062.html#263" class="Datatype">List</a> <a id="1043" href="Issue1062.html#965" class="Bound">A</a>
<a id="1045" class="Keyword">open</a> <a id="1050" href="Issue1062.html#958" class="Module">List1</a> <a id="1056" class="Keyword">using</a> <a id="1062" class="Symbol">(</a><a id="1063" href="Issue1062.html#1016" class="Field">head</a><a id="1067" class="Symbol">;</a> <a id="1069" href="Issue1062.html#1030" class="Field">tail</a><a id="1073" class="Symbol">)</a>

<a id="1076" class="Keyword">record</a> <a id="⊤"></a><a id="1083" href="Issue1062.html#1083" class="Record">⊤</a> <a id="1085" class="Symbol">:</a> <a id="1087" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="1091" class="Keyword">where</a> <a id="1097" class="Keyword">constructor</a> <a id="trivial"></a><a id="1109" href="Issue1062.html#1109" class="InductiveConstructor">trivial</a>
<a id="1117" class="Keyword">open</a> <a id="1122" href="Issue1062.html#958" class="Module">List1</a> <a id="1128" class="Symbol">(</a><a id="1129" href="Issue1062.html#1109" class="InductiveConstructor">trivial</a> <a id="1137" href="Issue1062.html#1000" class="InductiveConstructor Operator">∷</a> <a id="1139" href="Issue1062.html#292" class="InductiveConstructor">[]</a><a id="1141" class="Symbol">)</a> <a id="1143" class="Keyword">using</a> <a id="1149" class="Symbol">(</a><a id="1150" href="Issue1062.html#1016" class="Field">head</a><a id="1154" class="Symbol">;</a> <a id="1156" href="Issue1062.html#1030" class="Field">tail</a><a id="1160" class="Symbol">)</a> <a id="1162" class="Comment">-- problem: imports not colored</a>

<a id="unfold⁺"></a><a id="1195" href="Issue1062.html#1195" class="Function">unfold⁺</a> <a id="1203" class="Symbol">:</a> <a id="1205" class="Symbol">∀</a> <a id="1207" class="Symbol">{</a><a id="1208" href="Issue1062.html#1208" class="Bound">S</a> <a id="1210" class="Symbol">:</a> <a id="1212" href="Issue1062.html#153" class="Postulate">Size</a> <a id="1217" class="Symbol">→</a> <a id="1219" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="1222" class="Symbol">}</a> <a id="1224" class="Symbol">{</a><a id="1225" href="Issue1062.html#1225" class="Bound">A</a> <a id="1227" class="Symbol">:</a> <a id="1229" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="1232" class="Symbol">}</a>

  <a id="1237" class="Symbol">(</a><a id="1238" href="Issue1062.html#1238" class="Bound">step</a> <a id="1243" class="Symbol">:</a> <a id="1245" class="Symbol">∀</a> <a id="1247" class="Symbol">{</a><a id="1248" href="Issue1062.html#1248" class="Bound">i</a><a id="1249" class="Symbol">}</a> <a id="1251" class="Symbol">→</a> <a id="1253" href="Issue1062.html#1208" class="Bound">S</a> <a id="1255" href="Issue1062.html#1248" class="Bound">i</a> <a id="1257" class="Symbol">→</a> <a id="1259" href="Issue1062.html#958" class="Record">List1</a> <a id="1265" href="Issue1062.html#1225" class="Bound">A</a> <a id="1267" href="Issue1062.html#352" class="Record Operator">×</a> <a id="1269" class="Symbol">(∀</a> <a id="1272" class="Symbol">{</a><a id="1273" href="Issue1062.html#1273" class="Bound">j</a> <a id="1275" class="Symbol">:</a> <a id="1277" href="Issue1062.html#184" class="Postulate Operator">Size&lt;</a> <a id="1283" href="Issue1062.html#1248" class="Bound">i</a><a id="1284" class="Symbol">}</a> <a id="1286" class="Symbol">→</a> <a id="1288" href="Issue1062.html#1208" class="Bound">S</a> <a id="1290" href="Issue1062.html#1273" class="Bound">j</a><a id="1291" class="Symbol">))</a> <a id="1294" class="Symbol">→</a>

  <a id="1299" class="Symbol">∀</a> <a id="1301" class="Symbol">{</a><a id="1302" href="Issue1062.html#1302" class="Bound">i</a><a id="1303" class="Symbol">}</a> <a id="1305" class="Symbol">→</a> <a id="1307" class="Symbol">(</a><a id="1308" href="Issue1062.html#1308" class="Bound">s</a> <a id="1310" class="Symbol">:</a> <a id="1312" href="Issue1062.html#1208" class="Bound">S</a> <a id="1314" href="Issue1062.html#1302" class="Bound">i</a><a id="1315" class="Symbol">)</a> <a id="1317" class="Symbol">→</a> <a id="1319" href="Issue1062.html#480" class="Record">Stream</a> <a id="1326" class="Symbol">{</a><a id="1327" href="Issue1062.html#1302" class="Bound">i</a><a id="1328" class="Symbol">}</a> <a id="1330" href="Issue1062.html#1225" class="Bound">A</a>

<a id="1333" href="Issue1062.html#563" class="Field">head</a>  <a id="1339" class="Symbol">(</a><a id="1340" href="Issue1062.html#1195" class="Function">unfold⁺</a> <a id="1348" href="Issue1062.html#1348" class="Bound">step</a> <a id="1353" href="Issue1062.html#1353" class="Bound">s</a><a id="1354" class="Symbol">)</a> <a id="1356" class="Symbol">=</a>  <a id="1359" href="Issue1062.html#1016" class="Field">head</a> <a id="1364" class="Symbol">(</a><a id="1365" href="Issue1062.html#410" class="Field">fst</a> <a id="1369" class="Symbol">(</a><a id="1370" href="Issue1062.html#1348" class="Bound">step</a> <a id="1375" href="Issue1062.html#1353" class="Bound">s</a><a id="1376" class="Symbol">))</a>
<a id="1379" href="Issue1062.html#577" class="Field">tail</a>  <a id="1385" class="Symbol">(</a><a id="1386" href="Issue1062.html#1195" class="Function">unfold⁺</a> <a id="1394" href="Issue1062.html#1394" class="Bound">step</a> <a id="1399" href="Issue1062.html#1399" class="Bound">s</a><a id="1400" class="Symbol">)</a> <a id="1402" class="Symbol">=</a>  <a id="1405" class="Keyword">let</a>  <a id="1410" class="Symbol">((_</a> <a id="1414" href="Issue1062.html#1000" class="InductiveConstructor Operator">∷</a> <a id="1416" href="Issue1062.html#1416" class="Bound">l</a><a id="1417" class="Symbol">)</a> <a id="1419" href="Issue1062.html#394" class="InductiveConstructor Operator">,</a> <a id="1421" href="Issue1062.html#1421" class="Bound">s′</a><a id="1423" class="Symbol">)</a> <a id="1425" class="Symbol">=</a> <a id="1427" href="Issue1062.html#1394" class="Bound">step</a> <a id="1432" href="Issue1062.html#1399" class="Bound">s</a>
                          <a id="1460" class="Keyword">in</a>   <a id="1465" href="Issue1062.html#1416" class="Bound">l</a> <a id="1467" href="Issue1062.html#787" class="Function Operator">++ˢ</a> <a id="1471" href="Issue1062.html#1195" class="Function">unfold⁺</a> <a id="1479" href="Issue1062.html#1394" class="Bound">step</a> <a id="1484" href="Issue1062.html#1421" class="Bound">s′</a>
<a id="1487" class="Markup">\end{code}</a><a id="1497" class="Background">
Problem: The ∷ in the last let statement is not colored with constructor color.
\end{document}
</a></pre></body></html>